Section: New Results

Shape Analysis

We have extended the Xisa (eXtensible Inductive Shape Analysis) framework, in order to better deal with low level coding styles and programming languages, and in order to analyze recursive programs in a context dependent way. We also introduced a classification for semantic memory models.

Abstracting Calling-Context with Shapes

Participants : Bor-Yuh Evan Chang [University of Colorado at Boulder (USA)] , Xavier Rival.

Interprocedural program analysis is often performed by computing procedure summaries. While possible, computing adequate summaries is difficult, particularly in the presence of recursive procedures. In [23] , we propose a complementary framework for interprocedural analysis based on a direct abstraction of the calling context. Specifically, our approach exploits the inductive structure of a calling context by treating it directly as a stack of activation records. We built an abstraction based on separation logic with inductive definitions. A key element of this abstract domain is the use of parameters to refine the meaning of such call stack summaries and thus express relations across activation records and with the heap. In essence, we define an abstract interpretation-based analysis framework for recursive programs that permits a fluid per call site abstraction of the call stack—much like how shape analyzers enable a fluid per program point abstraction of the heap.

Abstract domains for the analysis of programs manipulating complex data-structures

Participant : Xavier Rival.

We proposed a framework for building abstract domains for the static analysis of programs which manipulate complex* data-structures [8] . Our abstract domain is parametric in the choice of a numerical abstract domain to represent properties of numeric memory cells and in the choice of a set of inductive definitions to be used in order to summarize unbounded heap regions. It features standard primitives for the computation of transfer functions, for the inclusion checking and for the computation of widening iterates. We also proposed an extension to handle programs that make use of low-level memory addressing, and proposed an extension of the widening to infer inductive definitions.

Composite abstract domain for the analysis of dynamic structures

Participants : Xavier Rival, Antoine Toubhans.

Reduced product is a general operation to combine abstract domains into more powerful abstract domains, which has been especially used to construct numerical abstract domains. However, until now, it has not been applied to memory structures. We proposed an instance of a reduced product operation, which can be applied on shape abstract domains based on separation logic and on inductive definitions. The advantage of this construction is that it allows to describe more complex heap dynamic data structures without making the design of all abstract operation more complex. In the other hand, it incurs a reduction cost, whenever we need to transport some information from one domain to the other. We showed that optimal reduction cannot be achieved, and identified the main source of complexity of this operation. A prototype implementation was also carried out. This work was done as part of Antoine Toubhans Master internship.